(0) Obligation:

Clauses:

div(X, Y, Z) :- quot(X, Y, Y, Z).
quot(0, s(Y), s(Z), R) :- ','(!, eq(R, 0)).
quot(X, 0, Z, U) :- ','(!, ','(eq(Z, s(X1)), ','(p(U, P), quot(X, Z, Z, P)))).
quot(s(X), Y, Z, U) :- ','(p(Y, P), quot(X, P, Z, U)).
p(0, 0).
p(s(X), X).
eq(X, X).

Query: div(g,g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

quotA(s(X1)) :- quotB(X1).
quotC(s(X1), X2) :- quotD(X1, X2).
quotD(X1, 0) :- quotA(X1).
quotD(X1, s(X2)) :- quotC(X1, X2).
quotE(s(s(X1))) :- quotF(X1).
quotG(s(s(X1)), X2) :- quotH(X1, X2).
quotH(X1, 0) :- quotE(X1).
quotH(X1, s(X2)) :- quotG(X1, X2).
quotI(s(s(s(X1)))) :- quotJ(X1).
quotK(s(s(s(X1))), X2) :- quotL(X1, X2).
quotL(X1, 0) :- quotI(X1).
quotL(X1, s(X2)) :- quotK(X1, X2).
quotM(s(s(s(s(X1))))) :- quotN(X1).
quotO(s(s(s(s(X1)))), X2) :- quotP(X1, X2).
quotP(X1, 0) :- quotM(X1).
quotP(X1, s(X2)) :- quotO(X1, X2).
quotQ(s(s(s(s(s(X1)))))) :- quotR(X1).
quotS(s(s(s(s(s(X1))))), X2) :- quotT(X1, X2).
quotT(X1, 0) :- quotQ(X1).
quotT(X1, s(X2)) :- quotS(X1, X2).
quotU(s(s(s(s(s(s(X1))))))) :- quotV(X1).
quotW(s(s(s(s(s(s(X1)))))), X2) :- quotX(X1, X2).
quotX(X1, 0) :- quotU(X1).
quotX(X1, s(X2)) :- quotW(X1, X2).
quotY(s(s(s(s(s(s(s(X1)))))))) :- quotZ(X1).
quotN1(s(s(s(s(s(s(s(X1))))))), X2) :- quotN2(X1, X2).
quotN2(X1, 0) :- quotY(X1).
quotN2(X1, s(X2)) :- quotN1(X1, X2).
quotB(X1) :- quotA(X1).
quotF(X1) :- quotE(X1).
quotJ(X1) :- quotI(X1).
quotN(X1) :- quotM(X1).
quotR(X1) :- quotQ(X1).
quotV(X1) :- quotU(X1).
quotZ(X1) :- quotY(X1).
quotN3(s(X1), 0) :- quotA(X1).
quotN3(s(s(X1)), 0) :- quotB(X1).
quotN3(s(s(X1)), s(0)) :- quotE(X1).
quotN3(s(s(s(X1))), s(0)) :- quotF(X1).
quotN3(s(s(s(X1))), s(s(0))) :- quotI(X1).
quotN3(s(s(s(s(X1)))), s(s(0))) :- quotJ(X1).
quotN3(s(s(s(s(X1)))), s(s(s(0)))) :- quotM(X1).
quotN3(s(s(s(s(s(X1))))), s(s(s(0)))) :- quotN(X1).
quotN3(s(s(s(s(s(X1))))), s(s(s(s(0))))) :- quotQ(X1).
quotN3(s(s(s(s(s(s(X1)))))), s(s(s(s(0))))) :- quotR(X1).
quotN3(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0)))))) :- quotU(X1).
quotN3(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(0)))))) :- quotV(X1).
quotN3(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0))))))) :- quotY(X1).
quotN3(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(0))))))) :- quotZ(X1).
quotN3(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) :- quotN4(X1, X2, s(s(s(s(s(s(s(X2)))))))).
quotN4(X1, 0, X2) :- quotN3(X1, X2).
quotN4(s(X1), 0, X2) :- quotN3(X1, X2).
quotN4(s(X1), s(X2), X3) :- quotN4(X1, X2, X3).
quotN5(s(X1), s(0), 0) :- quotA(X1).
quotN5(s(X1), s(0), s(X2)) :- quotC(X1, X2).
quotN5(s(s(X1)), s(0), X2) :- quotD(X1, X2).
quotN5(s(s(X1)), s(s(0)), 0) :- quotE(X1).
quotN5(s(s(X1)), s(s(0)), s(X2)) :- quotG(X1, X2).
quotN5(s(s(s(X1))), s(s(0)), X2) :- quotH(X1, X2).
quotN5(s(s(s(X1))), s(s(s(0))), 0) :- quotI(X1).
quotN5(s(s(s(X1))), s(s(s(0))), s(X2)) :- quotK(X1, X2).
quotN5(s(s(s(s(X1)))), s(s(s(0))), X2) :- quotL(X1, X2).
quotN5(s(s(s(s(X1)))), s(s(s(s(0)))), 0) :- quotM(X1).
quotN5(s(s(s(s(X1)))), s(s(s(s(0)))), s(X2)) :- quotO(X1, X2).
quotN5(s(s(s(s(s(X1))))), s(s(s(s(0)))), X2) :- quotP(X1, X2).
quotN5(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), 0) :- quotQ(X1).
quotN5(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), s(X2)) :- quotS(X1, X2).
quotN5(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0))))), X2) :- quotT(X1, X2).
quotN5(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), 0) :- quotU(X1).
quotN5(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), s(X2)) :- quotW(X1, X2).
quotN5(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0)))))), X2) :- quotX(X1, X2).
quotN5(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), 0) :- quotY(X1).
quotN5(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), s(X2)) :- quotN1(X1, X2).
quotN5(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(0))))))), X2) :- quotN2(X1, X2).
quotN5(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) :- quotN6(X1, X2, s(s(s(s(s(s(s(X2))))))), X3).
quotN6(X1, 0, X2, 0) :- quotN3(X1, X2).
quotN6(X1, 0, X2, s(X3)) :- quotN5(X1, s(X2), X3).
quotN6(s(X1), 0, X2, 0) :- quotN3(X1, X2).
quotN6(s(X1), 0, X2, s(X3)) :- quotN5(X1, s(X2), X3).
quotN6(s(X1), s(X2), X3, X4) :- quotN6(X1, X2, X3, X4).
divN7(X1, X2, X3) :- quotN5(X1, X2, X3).

Clauses:

quotcA(0).
quotcA(s(X1)) :- quotcB(X1).
quotcC(0, 0).
quotcC(s(X1), X2) :- quotcD(X1, X2).
quotcD(X1, 0) :- quotcA(X1).
quotcD(X1, s(X2)) :- quotcC(X1, X2).
quotcE(0).
quotcE(s(0)).
quotcE(s(s(X1))) :- quotcF(X1).
quotcG(0, 0).
quotcG(s(0), 0).
quotcG(s(s(X1)), X2) :- quotcH(X1, X2).
quotcH(X1, 0) :- quotcE(X1).
quotcH(X1, s(X2)) :- quotcG(X1, X2).
quotcI(0).
quotcI(s(0)).
quotcI(s(s(0))).
quotcI(s(s(s(X1)))) :- quotcJ(X1).
quotcK(0, 0).
quotcK(s(0), 0).
quotcK(s(s(0)), 0).
quotcK(s(s(s(X1))), X2) :- quotcL(X1, X2).
quotcL(X1, 0) :- quotcI(X1).
quotcL(X1, s(X2)) :- quotcK(X1, X2).
quotcM(0).
quotcM(s(0)).
quotcM(s(s(0))).
quotcM(s(s(s(0)))).
quotcM(s(s(s(s(X1))))) :- quotcN(X1).
quotcO(0, 0).
quotcO(s(0), 0).
quotcO(s(s(0)), 0).
quotcO(s(s(s(0))), 0).
quotcO(s(s(s(s(X1)))), X2) :- quotcP(X1, X2).
quotcP(X1, 0) :- quotcM(X1).
quotcP(X1, s(X2)) :- quotcO(X1, X2).
quotcQ(0).
quotcQ(s(0)).
quotcQ(s(s(0))).
quotcQ(s(s(s(0)))).
quotcQ(s(s(s(s(0))))).
quotcQ(s(s(s(s(s(X1)))))) :- quotcR(X1).
quotcS(0, 0).
quotcS(s(0), 0).
quotcS(s(s(0)), 0).
quotcS(s(s(s(0))), 0).
quotcS(s(s(s(s(0)))), 0).
quotcS(s(s(s(s(s(X1))))), X2) :- quotcT(X1, X2).
quotcT(X1, 0) :- quotcQ(X1).
quotcT(X1, s(X2)) :- quotcS(X1, X2).
quotcU(0).
quotcU(s(0)).
quotcU(s(s(0))).
quotcU(s(s(s(0)))).
quotcU(s(s(s(s(0))))).
quotcU(s(s(s(s(s(0)))))).
quotcU(s(s(s(s(s(s(X1))))))) :- quotcV(X1).
quotcW(0, 0).
quotcW(s(0), 0).
quotcW(s(s(0)), 0).
quotcW(s(s(s(0))), 0).
quotcW(s(s(s(s(0)))), 0).
quotcW(s(s(s(s(s(0))))), 0).
quotcW(s(s(s(s(s(s(X1)))))), X2) :- quotcX(X1, X2).
quotcX(X1, 0) :- quotcU(X1).
quotcX(X1, s(X2)) :- quotcW(X1, X2).
quotcY(0).
quotcY(s(0)).
quotcY(s(s(0))).
quotcY(s(s(s(0)))).
quotcY(s(s(s(s(0))))).
quotcY(s(s(s(s(s(0)))))).
quotcY(s(s(s(s(s(s(0))))))).
quotcY(s(s(s(s(s(s(s(X1)))))))) :- quotcZ(X1).
quotcN1(0, 0).
quotcN1(s(0), 0).
quotcN1(s(s(0)), 0).
quotcN1(s(s(s(0))), 0).
quotcN1(s(s(s(s(0)))), 0).
quotcN1(s(s(s(s(s(0))))), 0).
quotcN1(s(s(s(s(s(s(0)))))), 0).
quotcN1(s(s(s(s(s(s(s(X1))))))), X2) :- quotcN2(X1, X2).
quotcN2(X1, 0) :- quotcY(X1).
quotcN2(X1, s(X2)) :- quotcN1(X1, X2).
quotcB(X1) :- quotcA(X1).
quotcF(X1) :- quotcE(X1).
quotcJ(X1) :- quotcI(X1).
quotcN(X1) :- quotcM(X1).
quotcR(X1) :- quotcQ(X1).
quotcV(X1) :- quotcU(X1).
quotcZ(X1) :- quotcY(X1).
quotcN3(0, X1).
quotcN3(s(0), s(X1)).
quotcN3(s(X1), 0) :- quotcA(X1).
quotcN3(s(s(X1)), 0) :- quotcB(X1).
quotcN3(s(s(0)), s(s(X1))).
quotcN3(s(s(X1)), s(0)) :- quotcE(X1).
quotcN3(s(s(s(X1))), s(0)) :- quotcF(X1).
quotcN3(s(s(s(0))), s(s(s(X1)))).
quotcN3(s(s(s(X1))), s(s(0))) :- quotcI(X1).
quotcN3(s(s(s(s(X1)))), s(s(0))) :- quotcJ(X1).
quotcN3(s(s(s(s(0)))), s(s(s(s(X1))))).
quotcN3(s(s(s(s(X1)))), s(s(s(0)))) :- quotcM(X1).
quotcN3(s(s(s(s(s(X1))))), s(s(s(0)))) :- quotcN(X1).
quotcN3(s(s(s(s(s(0))))), s(s(s(s(s(X1)))))).
quotcN3(s(s(s(s(s(X1))))), s(s(s(s(0))))) :- quotcQ(X1).
quotcN3(s(s(s(s(s(s(X1)))))), s(s(s(s(0))))) :- quotcR(X1).
quotcN3(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(X1))))))).
quotcN3(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0)))))) :- quotcU(X1).
quotcN3(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(0)))))) :- quotcV(X1).
quotcN3(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(X1)))))))).
quotcN3(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0))))))) :- quotcY(X1).
quotcN3(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(0))))))) :- quotcZ(X1).
quotcN3(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) :- quotcN4(X1, X2, s(s(s(s(s(s(s(X2)))))))).
quotcN4(0, s(X1), X2).
quotcN4(X1, 0, X2) :- quotcN3(X1, X2).
quotcN4(s(X1), 0, X2) :- quotcN3(X1, X2).
quotcN4(s(X1), s(X2), X3) :- quotcN4(X1, X2, X3).
quotcN5(0, s(X1), 0).
quotcN5(s(0), s(s(X1)), 0).
quotcN5(s(X1), s(0), 0) :- quotcA(X1).
quotcN5(s(X1), s(0), s(X2)) :- quotcC(X1, X2).
quotcN5(s(s(X1)), s(0), X2) :- quotcD(X1, X2).
quotcN5(s(s(0)), s(s(s(X1))), 0).
quotcN5(s(s(X1)), s(s(0)), 0) :- quotcE(X1).
quotcN5(s(s(X1)), s(s(0)), s(X2)) :- quotcG(X1, X2).
quotcN5(s(s(s(X1))), s(s(0)), X2) :- quotcH(X1, X2).
quotcN5(s(s(s(0))), s(s(s(s(X1)))), 0).
quotcN5(s(s(s(X1))), s(s(s(0))), 0) :- quotcI(X1).
quotcN5(s(s(s(X1))), s(s(s(0))), s(X2)) :- quotcK(X1, X2).
quotcN5(s(s(s(s(X1)))), s(s(s(0))), X2) :- quotcL(X1, X2).
quotcN5(s(s(s(s(0)))), s(s(s(s(s(X1))))), 0).
quotcN5(s(s(s(s(X1)))), s(s(s(s(0)))), 0) :- quotcM(X1).
quotcN5(s(s(s(s(X1)))), s(s(s(s(0)))), s(X2)) :- quotcO(X1, X2).
quotcN5(s(s(s(s(s(X1))))), s(s(s(s(0)))), X2) :- quotcP(X1, X2).
quotcN5(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))), 0).
quotcN5(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), 0) :- quotcQ(X1).
quotcN5(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), s(X2)) :- quotcS(X1, X2).
quotcN5(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0))))), X2) :- quotcT(X1, X2).
quotcN5(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))), 0).
quotcN5(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), 0) :- quotcU(X1).
quotcN5(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), s(X2)) :- quotcW(X1, X2).
quotcN5(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0)))))), X2) :- quotcX(X1, X2).
quotcN5(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(X1)))))))), 0).
quotcN5(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), 0) :- quotcY(X1).
quotcN5(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), s(X2)) :- quotcN1(X1, X2).
quotcN5(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(0))))))), X2) :- quotcN2(X1, X2).
quotcN5(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) :- quotcN6(X1, X2, s(s(s(s(s(s(s(X2))))))), X3).
quotcN6(0, s(X1), X2, 0).
quotcN6(X1, 0, X2, 0) :- quotcN3(X1, X2).
quotcN6(X1, 0, X2, s(X3)) :- quotcN5(X1, s(X2), X3).
quotcN6(s(X1), 0, X2, 0) :- quotcN3(X1, X2).
quotcN6(s(X1), 0, X2, s(X3)) :- quotcN5(X1, s(X2), X3).
quotcN6(s(X1), s(X2), X3, X4) :- quotcN6(X1, X2, X3, X4).

Afs:

divN7(x1, x2, x3)  =  divN7(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
divN7_in: (b,b,f)
quotN5_in: (b,b,f)
quotA_in: (b)
quotB_in: (b)
quotC_in: (b,f)
quotD_in: (b,f)
quotE_in: (b)
quotF_in: (b)
quotG_in: (b,f)
quotH_in: (b,f)
quotI_in: (b)
quotJ_in: (b)
quotK_in: (b,f)
quotL_in: (b,f)
quotM_in: (b)
quotN_in: (b)
quotO_in: (b,f)
quotP_in: (b,f)
quotQ_in: (b)
quotR_in: (b)
quotS_in: (b,f)
quotT_in: (b,f)
quotU_in: (b)
quotV_in: (b)
quotW_in: (b,f)
quotX_in: (b,f)
quotY_in: (b)
quotZ_in: (b)
quotN1_in: (b,f)
quotN2_in: (b,f)
quotN6_in: (b,b,b,f)
quotN3_in: (b,b)
quotN4_in: (b,b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

DIVN7_IN_GGA(X1, X2, X3) → U81_GGA(X1, X2, X3, quotN5_in_gga(X1, X2, X3))
DIVN7_IN_GGA(X1, X2, X3) → QUOTN5_IN_GGA(X1, X2, X3)
QUOTN5_IN_GGA(s(X1), s(0), 0) → U54_GGA(X1, quotA_in_g(X1))
QUOTN5_IN_GGA(s(X1), s(0), 0) → QUOTA_IN_G(X1)
QUOTA_IN_G(s(X1)) → U1_G(X1, quotB_in_g(X1))
QUOTA_IN_G(s(X1)) → QUOTB_IN_G(X1)
QUOTB_IN_G(X1) → U29_G(X1, quotA_in_g(X1))
QUOTB_IN_G(X1) → QUOTA_IN_G(X1)
QUOTN5_IN_GGA(s(X1), s(0), s(X2)) → U55_GGA(X1, X2, quotC_in_ga(X1, X2))
QUOTN5_IN_GGA(s(X1), s(0), s(X2)) → QUOTC_IN_GA(X1, X2)
QUOTC_IN_GA(s(X1), X2) → U2_GA(X1, X2, quotD_in_ga(X1, X2))
QUOTC_IN_GA(s(X1), X2) → QUOTD_IN_GA(X1, X2)
QUOTD_IN_GA(X1, 0) → U3_GA(X1, quotA_in_g(X1))
QUOTD_IN_GA(X1, 0) → QUOTA_IN_G(X1)
QUOTD_IN_GA(X1, s(X2)) → U4_GA(X1, X2, quotC_in_ga(X1, X2))
QUOTD_IN_GA(X1, s(X2)) → QUOTC_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(X1)), s(0), X2) → U56_GGA(X1, X2, quotD_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(X1)), s(0), X2) → QUOTD_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), 0) → U57_GGA(X1, quotE_in_g(X1))
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), 0) → QUOTE_IN_G(X1)
QUOTE_IN_G(s(s(X1))) → U5_G(X1, quotF_in_g(X1))
QUOTE_IN_G(s(s(X1))) → QUOTF_IN_G(X1)
QUOTF_IN_G(X1) → U30_G(X1, quotE_in_g(X1))
QUOTF_IN_G(X1) → QUOTE_IN_G(X1)
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), s(X2)) → U58_GGA(X1, X2, quotG_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), s(X2)) → QUOTG_IN_GA(X1, X2)
QUOTG_IN_GA(s(s(X1)), X2) → U6_GA(X1, X2, quotH_in_ga(X1, X2))
QUOTG_IN_GA(s(s(X1)), X2) → QUOTH_IN_GA(X1, X2)
QUOTH_IN_GA(X1, 0) → U7_GA(X1, quotE_in_g(X1))
QUOTH_IN_GA(X1, 0) → QUOTE_IN_G(X1)
QUOTH_IN_GA(X1, s(X2)) → U8_GA(X1, X2, quotG_in_ga(X1, X2))
QUOTH_IN_GA(X1, s(X2)) → QUOTG_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(X1))), s(s(0)), X2) → U59_GGA(X1, X2, quotH_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(X1))), s(s(0)), X2) → QUOTH_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), 0) → U60_GGA(X1, quotI_in_g(X1))
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), 0) → QUOTI_IN_G(X1)
QUOTI_IN_G(s(s(s(X1)))) → U9_G(X1, quotJ_in_g(X1))
QUOTI_IN_G(s(s(s(X1)))) → QUOTJ_IN_G(X1)
QUOTJ_IN_G(X1) → U31_G(X1, quotI_in_g(X1))
QUOTJ_IN_G(X1) → QUOTI_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), s(X2)) → U61_GGA(X1, X2, quotK_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), s(X2)) → QUOTK_IN_GA(X1, X2)
QUOTK_IN_GA(s(s(s(X1))), X2) → U10_GA(X1, X2, quotL_in_ga(X1, X2))
QUOTK_IN_GA(s(s(s(X1))), X2) → QUOTL_IN_GA(X1, X2)
QUOTL_IN_GA(X1, 0) → U11_GA(X1, quotI_in_g(X1))
QUOTL_IN_GA(X1, 0) → QUOTI_IN_G(X1)
QUOTL_IN_GA(X1, s(X2)) → U12_GA(X1, X2, quotK_in_ga(X1, X2))
QUOTL_IN_GA(X1, s(X2)) → QUOTK_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(0))), X2) → U62_GGA(X1, X2, quotL_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(0))), X2) → QUOTL_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), 0) → U63_GGA(X1, quotM_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), 0) → QUOTM_IN_G(X1)
QUOTM_IN_G(s(s(s(s(X1))))) → U13_G(X1, quotN_in_g(X1))
QUOTM_IN_G(s(s(s(s(X1))))) → QUOTN_IN_G(X1)
QUOTN_IN_G(X1) → U32_G(X1, quotM_in_g(X1))
QUOTN_IN_G(X1) → QUOTM_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), s(X2)) → U64_GGA(X1, X2, quotO_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), s(X2)) → QUOTO_IN_GA(X1, X2)
QUOTO_IN_GA(s(s(s(s(X1)))), X2) → U14_GA(X1, X2, quotP_in_ga(X1, X2))
QUOTO_IN_GA(s(s(s(s(X1)))), X2) → QUOTP_IN_GA(X1, X2)
QUOTP_IN_GA(X1, 0) → U15_GA(X1, quotM_in_g(X1))
QUOTP_IN_GA(X1, 0) → QUOTM_IN_G(X1)
QUOTP_IN_GA(X1, s(X2)) → U16_GA(X1, X2, quotO_in_ga(X1, X2))
QUOTP_IN_GA(X1, s(X2)) → QUOTO_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(0)))), X2) → U65_GGA(X1, X2, quotP_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(0)))), X2) → QUOTP_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), 0) → U66_GGA(X1, quotQ_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), 0) → QUOTQ_IN_G(X1)
QUOTQ_IN_G(s(s(s(s(s(X1)))))) → U17_G(X1, quotR_in_g(X1))
QUOTQ_IN_G(s(s(s(s(s(X1)))))) → QUOTR_IN_G(X1)
QUOTR_IN_G(X1) → U33_G(X1, quotQ_in_g(X1))
QUOTR_IN_G(X1) → QUOTQ_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), s(X2)) → U67_GGA(X1, X2, quotS_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), s(X2)) → QUOTS_IN_GA(X1, X2)
QUOTS_IN_GA(s(s(s(s(s(X1))))), X2) → U18_GA(X1, X2, quotT_in_ga(X1, X2))
QUOTS_IN_GA(s(s(s(s(s(X1))))), X2) → QUOTT_IN_GA(X1, X2)
QUOTT_IN_GA(X1, 0) → U19_GA(X1, quotQ_in_g(X1))
QUOTT_IN_GA(X1, 0) → QUOTQ_IN_G(X1)
QUOTT_IN_GA(X1, s(X2)) → U20_GA(X1, X2, quotS_in_ga(X1, X2))
QUOTT_IN_GA(X1, s(X2)) → QUOTS_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0))))), X2) → U68_GGA(X1, X2, quotT_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0))))), X2) → QUOTT_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), 0) → U69_GGA(X1, quotU_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), 0) → QUOTU_IN_G(X1)
QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → U21_G(X1, quotV_in_g(X1))
QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → QUOTV_IN_G(X1)
QUOTV_IN_G(X1) → U34_G(X1, quotU_in_g(X1))
QUOTV_IN_G(X1) → QUOTU_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), s(X2)) → U70_GGA(X1, X2, quotW_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), s(X2)) → QUOTW_IN_GA(X1, X2)
QUOTW_IN_GA(s(s(s(s(s(s(X1)))))), X2) → U22_GA(X1, X2, quotX_in_ga(X1, X2))
QUOTW_IN_GA(s(s(s(s(s(s(X1)))))), X2) → QUOTX_IN_GA(X1, X2)
QUOTX_IN_GA(X1, 0) → U23_GA(X1, quotU_in_g(X1))
QUOTX_IN_GA(X1, 0) → QUOTU_IN_G(X1)
QUOTX_IN_GA(X1, s(X2)) → U24_GA(X1, X2, quotW_in_ga(X1, X2))
QUOTX_IN_GA(X1, s(X2)) → QUOTW_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0)))))), X2) → U71_GGA(X1, X2, quotX_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0)))))), X2) → QUOTX_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), 0) → U72_GGA(X1, quotY_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), 0) → QUOTY_IN_G(X1)
QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → U25_G(X1, quotZ_in_g(X1))
QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → QUOTZ_IN_G(X1)
QUOTZ_IN_G(X1) → U35_G(X1, quotY_in_g(X1))
QUOTZ_IN_G(X1) → QUOTY_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), s(X2)) → U73_GGA(X1, X2, quotN1_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), s(X2)) → QUOTN1_IN_GA(X1, X2)
QUOTN1_IN_GA(s(s(s(s(s(s(s(X1))))))), X2) → U26_GA(X1, X2, quotN2_in_ga(X1, X2))
QUOTN1_IN_GA(s(s(s(s(s(s(s(X1))))))), X2) → QUOTN2_IN_GA(X1, X2)
QUOTN2_IN_GA(X1, 0) → U27_GA(X1, quotY_in_g(X1))
QUOTN2_IN_GA(X1, 0) → QUOTY_IN_G(X1)
QUOTN2_IN_GA(X1, s(X2)) → U28_GA(X1, X2, quotN1_in_ga(X1, X2))
QUOTN2_IN_GA(X1, s(X2)) → QUOTN1_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(0))))))), X2) → U74_GGA(X1, X2, quotN2_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(0))))))), X2) → QUOTN2_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) → U75_GGA(X1, X2, X3, quotN6_in_ggga(X1, X2, s(s(s(s(s(s(s(X2))))))), X3))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) → QUOTN6_IN_GGGA(X1, X2, s(s(s(s(s(s(s(X2))))))), X3)
QUOTN6_IN_GGGA(X1, 0, X2, 0) → U76_GGGA(X1, X2, quotN3_in_gg(X1, X2))
QUOTN6_IN_GGGA(X1, 0, X2, 0) → QUOTN3_IN_GG(X1, X2)
QUOTN3_IN_GG(s(X1), 0) → U36_GG(X1, quotA_in_g(X1))
QUOTN3_IN_GG(s(X1), 0) → QUOTA_IN_G(X1)
QUOTN3_IN_GG(s(s(X1)), 0) → U37_GG(X1, quotB_in_g(X1))
QUOTN3_IN_GG(s(s(X1)), 0) → QUOTB_IN_G(X1)
QUOTN3_IN_GG(s(s(X1)), s(0)) → U38_GG(X1, quotE_in_g(X1))
QUOTN3_IN_GG(s(s(X1)), s(0)) → QUOTE_IN_G(X1)
QUOTN3_IN_GG(s(s(s(X1))), s(0)) → U39_GG(X1, quotF_in_g(X1))
QUOTN3_IN_GG(s(s(s(X1))), s(0)) → QUOTF_IN_G(X1)
QUOTN3_IN_GG(s(s(s(X1))), s(s(0))) → U40_GG(X1, quotI_in_g(X1))
QUOTN3_IN_GG(s(s(s(X1))), s(s(0))) → QUOTI_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(0))) → U41_GG(X1, quotJ_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(0))) → QUOTJ_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(s(0)))) → U42_GG(X1, quotM_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(s(0)))) → QUOTM_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(0)))) → U43_GG(X1, quotN_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(0)))) → QUOTN_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(s(0))))) → U44_GG(X1, quotQ_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(s(0))))) → QUOTQ_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(0))))) → U45_GG(X1, quotR_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(0))))) → QUOTR_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0)))))) → U46_GG(X1, quotU_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0)))))) → QUOTU_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(0)))))) → U47_GG(X1, quotV_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(0)))))) → QUOTV_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0))))))) → U48_GG(X1, quotY_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0))))))) → QUOTY_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(0))))))) → U49_GG(X1, quotZ_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(0))))))) → QUOTZ_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → U50_GG(X1, X2, quotN4_in_ggg(X1, X2, s(s(s(s(s(s(s(X2)))))))))
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → QUOTN4_IN_GGG(X1, X2, s(s(s(s(s(s(s(X2))))))))
QUOTN4_IN_GGG(X1, 0, X2) → U51_GGG(X1, X2, quotN3_in_gg(X1, X2))
QUOTN4_IN_GGG(X1, 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), 0, X2) → U52_GGG(X1, X2, quotN3_in_gg(X1, X2))
QUOTN4_IN_GGG(s(X1), 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), s(X2), X3) → U53_GGG(X1, X2, X3, quotN4_in_ggg(X1, X2, X3))
QUOTN4_IN_GGG(s(X1), s(X2), X3) → QUOTN4_IN_GGG(X1, X2, X3)
QUOTN6_IN_GGGA(X1, 0, X2, s(X3)) → U77_GGGA(X1, X2, X3, quotN5_in_gga(X1, s(X2), X3))
QUOTN6_IN_GGGA(X1, 0, X2, s(X3)) → QUOTN5_IN_GGA(X1, s(X2), X3)
QUOTN6_IN_GGGA(s(X1), 0, X2, 0) → U78_GGGA(X1, X2, quotN3_in_gg(X1, X2))
QUOTN6_IN_GGGA(s(X1), 0, X2, 0) → QUOTN3_IN_GG(X1, X2)
QUOTN6_IN_GGGA(s(X1), 0, X2, s(X3)) → U79_GGGA(X1, X2, X3, quotN5_in_gga(X1, s(X2), X3))
QUOTN6_IN_GGGA(s(X1), 0, X2, s(X3)) → QUOTN5_IN_GGA(X1, s(X2), X3)
QUOTN6_IN_GGGA(s(X1), s(X2), X3, X4) → U80_GGGA(X1, X2, X3, X4, quotN6_in_ggga(X1, X2, X3, X4))
QUOTN6_IN_GGGA(s(X1), s(X2), X3, X4) → QUOTN6_IN_GGGA(X1, X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
quotN5_in_gga(x1, x2, x3)  =  quotN5_in_gga(x1, x2)
s(x1)  =  s(x1)
0  =  0
quotA_in_g(x1)  =  quotA_in_g(x1)
quotB_in_g(x1)  =  quotB_in_g(x1)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotE_in_g(x1)  =  quotE_in_g(x1)
quotF_in_g(x1)  =  quotF_in_g(x1)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotI_in_g(x1)  =  quotI_in_g(x1)
quotJ_in_g(x1)  =  quotJ_in_g(x1)
quotK_in_ga(x1, x2)  =  quotK_in_ga(x1)
quotL_in_ga(x1, x2)  =  quotL_in_ga(x1)
quotM_in_g(x1)  =  quotM_in_g(x1)
quotN_in_g(x1)  =  quotN_in_g(x1)
quotO_in_ga(x1, x2)  =  quotO_in_ga(x1)
quotP_in_ga(x1, x2)  =  quotP_in_ga(x1)
quotQ_in_g(x1)  =  quotQ_in_g(x1)
quotR_in_g(x1)  =  quotR_in_g(x1)
quotS_in_ga(x1, x2)  =  quotS_in_ga(x1)
quotT_in_ga(x1, x2)  =  quotT_in_ga(x1)
quotU_in_g(x1)  =  quotU_in_g(x1)
quotV_in_g(x1)  =  quotV_in_g(x1)
quotW_in_ga(x1, x2)  =  quotW_in_ga(x1)
quotX_in_ga(x1, x2)  =  quotX_in_ga(x1)
quotY_in_g(x1)  =  quotY_in_g(x1)
quotZ_in_g(x1)  =  quotZ_in_g(x1)
quotN1_in_ga(x1, x2)  =  quotN1_in_ga(x1)
quotN2_in_ga(x1, x2)  =  quotN2_in_ga(x1)
quotN6_in_ggga(x1, x2, x3, x4)  =  quotN6_in_ggga(x1, x2, x3)
quotN3_in_gg(x1, x2)  =  quotN3_in_gg(x1, x2)
quotN4_in_ggg(x1, x2, x3)  =  quotN4_in_ggg(x1, x2, x3)
DIVN7_IN_GGA(x1, x2, x3)  =  DIVN7_IN_GGA(x1, x2)
U81_GGA(x1, x2, x3, x4)  =  U81_GGA(x1, x2, x4)
QUOTN5_IN_GGA(x1, x2, x3)  =  QUOTN5_IN_GGA(x1, x2)
U54_GGA(x1, x2)  =  U54_GGA(x1, x2)
QUOTA_IN_G(x1)  =  QUOTA_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
QUOTB_IN_G(x1)  =  QUOTB_IN_G(x1)
U29_G(x1, x2)  =  U29_G(x1, x2)
U55_GGA(x1, x2, x3)  =  U55_GGA(x1, x3)
QUOTC_IN_GA(x1, x2)  =  QUOTC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)
U3_GA(x1, x2)  =  U3_GA(x1, x2)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U56_GGA(x1, x2, x3)  =  U56_GGA(x1, x3)
U57_GGA(x1, x2)  =  U57_GGA(x1, x2)
QUOTE_IN_G(x1)  =  QUOTE_IN_G(x1)
U5_G(x1, x2)  =  U5_G(x1, x2)
QUOTF_IN_G(x1)  =  QUOTF_IN_G(x1)
U30_G(x1, x2)  =  U30_G(x1, x2)
U58_GGA(x1, x2, x3)  =  U58_GGA(x1, x3)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
QUOTH_IN_GA(x1, x2)  =  QUOTH_IN_GA(x1)
U7_GA(x1, x2)  =  U7_GA(x1, x2)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U59_GGA(x1, x2, x3)  =  U59_GGA(x1, x3)
U60_GGA(x1, x2)  =  U60_GGA(x1, x2)
QUOTI_IN_G(x1)  =  QUOTI_IN_G(x1)
U9_G(x1, x2)  =  U9_G(x1, x2)
QUOTJ_IN_G(x1)  =  QUOTJ_IN_G(x1)
U31_G(x1, x2)  =  U31_G(x1, x2)
U61_GGA(x1, x2, x3)  =  U61_GGA(x1, x3)
QUOTK_IN_GA(x1, x2)  =  QUOTK_IN_GA(x1)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
QUOTL_IN_GA(x1, x2)  =  QUOTL_IN_GA(x1)
U11_GA(x1, x2)  =  U11_GA(x1, x2)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U62_GGA(x1, x2, x3)  =  U62_GGA(x1, x3)
U63_GGA(x1, x2)  =  U63_GGA(x1, x2)
QUOTM_IN_G(x1)  =  QUOTM_IN_G(x1)
U13_G(x1, x2)  =  U13_G(x1, x2)
QUOTN_IN_G(x1)  =  QUOTN_IN_G(x1)
U32_G(x1, x2)  =  U32_G(x1, x2)
U64_GGA(x1, x2, x3)  =  U64_GGA(x1, x3)
QUOTO_IN_GA(x1, x2)  =  QUOTO_IN_GA(x1)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
QUOTP_IN_GA(x1, x2)  =  QUOTP_IN_GA(x1)
U15_GA(x1, x2)  =  U15_GA(x1, x2)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
U65_GGA(x1, x2, x3)  =  U65_GGA(x1, x3)
U66_GGA(x1, x2)  =  U66_GGA(x1, x2)
QUOTQ_IN_G(x1)  =  QUOTQ_IN_G(x1)
U17_G(x1, x2)  =  U17_G(x1, x2)
QUOTR_IN_G(x1)  =  QUOTR_IN_G(x1)
U33_G(x1, x2)  =  U33_G(x1, x2)
U67_GGA(x1, x2, x3)  =  U67_GGA(x1, x3)
QUOTS_IN_GA(x1, x2)  =  QUOTS_IN_GA(x1)
U18_GA(x1, x2, x3)  =  U18_GA(x1, x3)
QUOTT_IN_GA(x1, x2)  =  QUOTT_IN_GA(x1)
U19_GA(x1, x2)  =  U19_GA(x1, x2)
U20_GA(x1, x2, x3)  =  U20_GA(x1, x3)
U68_GGA(x1, x2, x3)  =  U68_GGA(x1, x3)
U69_GGA(x1, x2)  =  U69_GGA(x1, x2)
QUOTU_IN_G(x1)  =  QUOTU_IN_G(x1)
U21_G(x1, x2)  =  U21_G(x1, x2)
QUOTV_IN_G(x1)  =  QUOTV_IN_G(x1)
U34_G(x1, x2)  =  U34_G(x1, x2)
U70_GGA(x1, x2, x3)  =  U70_GGA(x1, x3)
QUOTW_IN_GA(x1, x2)  =  QUOTW_IN_GA(x1)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
QUOTX_IN_GA(x1, x2)  =  QUOTX_IN_GA(x1)
U23_GA(x1, x2)  =  U23_GA(x1, x2)
U24_GA(x1, x2, x3)  =  U24_GA(x1, x3)
U71_GGA(x1, x2, x3)  =  U71_GGA(x1, x3)
U72_GGA(x1, x2)  =  U72_GGA(x1, x2)
QUOTY_IN_G(x1)  =  QUOTY_IN_G(x1)
U25_G(x1, x2)  =  U25_G(x1, x2)
QUOTZ_IN_G(x1)  =  QUOTZ_IN_G(x1)
U35_G(x1, x2)  =  U35_G(x1, x2)
U73_GGA(x1, x2, x3)  =  U73_GGA(x1, x3)
QUOTN1_IN_GA(x1, x2)  =  QUOTN1_IN_GA(x1)
U26_GA(x1, x2, x3)  =  U26_GA(x1, x3)
QUOTN2_IN_GA(x1, x2)  =  QUOTN2_IN_GA(x1)
U27_GA(x1, x2)  =  U27_GA(x1, x2)
U28_GA(x1, x2, x3)  =  U28_GA(x1, x3)
U74_GGA(x1, x2, x3)  =  U74_GGA(x1, x3)
U75_GGA(x1, x2, x3, x4)  =  U75_GGA(x1, x2, x4)
QUOTN6_IN_GGGA(x1, x2, x3, x4)  =  QUOTN6_IN_GGGA(x1, x2, x3)
U76_GGGA(x1, x2, x3)  =  U76_GGGA(x1, x2, x3)
QUOTN3_IN_GG(x1, x2)  =  QUOTN3_IN_GG(x1, x2)
U36_GG(x1, x2)  =  U36_GG(x1, x2)
U37_GG(x1, x2)  =  U37_GG(x1, x2)
U38_GG(x1, x2)  =  U38_GG(x1, x2)
U39_GG(x1, x2)  =  U39_GG(x1, x2)
U40_GG(x1, x2)  =  U40_GG(x1, x2)
U41_GG(x1, x2)  =  U41_GG(x1, x2)
U42_GG(x1, x2)  =  U42_GG(x1, x2)
U43_GG(x1, x2)  =  U43_GG(x1, x2)
U44_GG(x1, x2)  =  U44_GG(x1, x2)
U45_GG(x1, x2)  =  U45_GG(x1, x2)
U46_GG(x1, x2)  =  U46_GG(x1, x2)
U47_GG(x1, x2)  =  U47_GG(x1, x2)
U48_GG(x1, x2)  =  U48_GG(x1, x2)
U49_GG(x1, x2)  =  U49_GG(x1, x2)
U50_GG(x1, x2, x3)  =  U50_GG(x1, x2, x3)
QUOTN4_IN_GGG(x1, x2, x3)  =  QUOTN4_IN_GGG(x1, x2, x3)
U51_GGG(x1, x2, x3)  =  U51_GGG(x1, x2, x3)
U52_GGG(x1, x2, x3)  =  U52_GGG(x1, x2, x3)
U53_GGG(x1, x2, x3, x4)  =  U53_GGG(x1, x2, x3, x4)
U77_GGGA(x1, x2, x3, x4)  =  U77_GGGA(x1, x2, x4)
U78_GGGA(x1, x2, x3)  =  U78_GGGA(x1, x2, x3)
U79_GGGA(x1, x2, x3, x4)  =  U79_GGGA(x1, x2, x4)
U80_GGGA(x1, x2, x3, x4, x5)  =  U80_GGGA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DIVN7_IN_GGA(X1, X2, X3) → U81_GGA(X1, X2, X3, quotN5_in_gga(X1, X2, X3))
DIVN7_IN_GGA(X1, X2, X3) → QUOTN5_IN_GGA(X1, X2, X3)
QUOTN5_IN_GGA(s(X1), s(0), 0) → U54_GGA(X1, quotA_in_g(X1))
QUOTN5_IN_GGA(s(X1), s(0), 0) → QUOTA_IN_G(X1)
QUOTA_IN_G(s(X1)) → U1_G(X1, quotB_in_g(X1))
QUOTA_IN_G(s(X1)) → QUOTB_IN_G(X1)
QUOTB_IN_G(X1) → U29_G(X1, quotA_in_g(X1))
QUOTB_IN_G(X1) → QUOTA_IN_G(X1)
QUOTN5_IN_GGA(s(X1), s(0), s(X2)) → U55_GGA(X1, X2, quotC_in_ga(X1, X2))
QUOTN5_IN_GGA(s(X1), s(0), s(X2)) → QUOTC_IN_GA(X1, X2)
QUOTC_IN_GA(s(X1), X2) → U2_GA(X1, X2, quotD_in_ga(X1, X2))
QUOTC_IN_GA(s(X1), X2) → QUOTD_IN_GA(X1, X2)
QUOTD_IN_GA(X1, 0) → U3_GA(X1, quotA_in_g(X1))
QUOTD_IN_GA(X1, 0) → QUOTA_IN_G(X1)
QUOTD_IN_GA(X1, s(X2)) → U4_GA(X1, X2, quotC_in_ga(X1, X2))
QUOTD_IN_GA(X1, s(X2)) → QUOTC_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(X1)), s(0), X2) → U56_GGA(X1, X2, quotD_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(X1)), s(0), X2) → QUOTD_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), 0) → U57_GGA(X1, quotE_in_g(X1))
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), 0) → QUOTE_IN_G(X1)
QUOTE_IN_G(s(s(X1))) → U5_G(X1, quotF_in_g(X1))
QUOTE_IN_G(s(s(X1))) → QUOTF_IN_G(X1)
QUOTF_IN_G(X1) → U30_G(X1, quotE_in_g(X1))
QUOTF_IN_G(X1) → QUOTE_IN_G(X1)
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), s(X2)) → U58_GGA(X1, X2, quotG_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), s(X2)) → QUOTG_IN_GA(X1, X2)
QUOTG_IN_GA(s(s(X1)), X2) → U6_GA(X1, X2, quotH_in_ga(X1, X2))
QUOTG_IN_GA(s(s(X1)), X2) → QUOTH_IN_GA(X1, X2)
QUOTH_IN_GA(X1, 0) → U7_GA(X1, quotE_in_g(X1))
QUOTH_IN_GA(X1, 0) → QUOTE_IN_G(X1)
QUOTH_IN_GA(X1, s(X2)) → U8_GA(X1, X2, quotG_in_ga(X1, X2))
QUOTH_IN_GA(X1, s(X2)) → QUOTG_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(X1))), s(s(0)), X2) → U59_GGA(X1, X2, quotH_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(X1))), s(s(0)), X2) → QUOTH_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), 0) → U60_GGA(X1, quotI_in_g(X1))
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), 0) → QUOTI_IN_G(X1)
QUOTI_IN_G(s(s(s(X1)))) → U9_G(X1, quotJ_in_g(X1))
QUOTI_IN_G(s(s(s(X1)))) → QUOTJ_IN_G(X1)
QUOTJ_IN_G(X1) → U31_G(X1, quotI_in_g(X1))
QUOTJ_IN_G(X1) → QUOTI_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), s(X2)) → U61_GGA(X1, X2, quotK_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), s(X2)) → QUOTK_IN_GA(X1, X2)
QUOTK_IN_GA(s(s(s(X1))), X2) → U10_GA(X1, X2, quotL_in_ga(X1, X2))
QUOTK_IN_GA(s(s(s(X1))), X2) → QUOTL_IN_GA(X1, X2)
QUOTL_IN_GA(X1, 0) → U11_GA(X1, quotI_in_g(X1))
QUOTL_IN_GA(X1, 0) → QUOTI_IN_G(X1)
QUOTL_IN_GA(X1, s(X2)) → U12_GA(X1, X2, quotK_in_ga(X1, X2))
QUOTL_IN_GA(X1, s(X2)) → QUOTK_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(0))), X2) → U62_GGA(X1, X2, quotL_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(0))), X2) → QUOTL_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), 0) → U63_GGA(X1, quotM_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), 0) → QUOTM_IN_G(X1)
QUOTM_IN_G(s(s(s(s(X1))))) → U13_G(X1, quotN_in_g(X1))
QUOTM_IN_G(s(s(s(s(X1))))) → QUOTN_IN_G(X1)
QUOTN_IN_G(X1) → U32_G(X1, quotM_in_g(X1))
QUOTN_IN_G(X1) → QUOTM_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), s(X2)) → U64_GGA(X1, X2, quotO_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), s(X2)) → QUOTO_IN_GA(X1, X2)
QUOTO_IN_GA(s(s(s(s(X1)))), X2) → U14_GA(X1, X2, quotP_in_ga(X1, X2))
QUOTO_IN_GA(s(s(s(s(X1)))), X2) → QUOTP_IN_GA(X1, X2)
QUOTP_IN_GA(X1, 0) → U15_GA(X1, quotM_in_g(X1))
QUOTP_IN_GA(X1, 0) → QUOTM_IN_G(X1)
QUOTP_IN_GA(X1, s(X2)) → U16_GA(X1, X2, quotO_in_ga(X1, X2))
QUOTP_IN_GA(X1, s(X2)) → QUOTO_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(0)))), X2) → U65_GGA(X1, X2, quotP_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(0)))), X2) → QUOTP_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), 0) → U66_GGA(X1, quotQ_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), 0) → QUOTQ_IN_G(X1)
QUOTQ_IN_G(s(s(s(s(s(X1)))))) → U17_G(X1, quotR_in_g(X1))
QUOTQ_IN_G(s(s(s(s(s(X1)))))) → QUOTR_IN_G(X1)
QUOTR_IN_G(X1) → U33_G(X1, quotQ_in_g(X1))
QUOTR_IN_G(X1) → QUOTQ_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), s(X2)) → U67_GGA(X1, X2, quotS_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), s(X2)) → QUOTS_IN_GA(X1, X2)
QUOTS_IN_GA(s(s(s(s(s(X1))))), X2) → U18_GA(X1, X2, quotT_in_ga(X1, X2))
QUOTS_IN_GA(s(s(s(s(s(X1))))), X2) → QUOTT_IN_GA(X1, X2)
QUOTT_IN_GA(X1, 0) → U19_GA(X1, quotQ_in_g(X1))
QUOTT_IN_GA(X1, 0) → QUOTQ_IN_G(X1)
QUOTT_IN_GA(X1, s(X2)) → U20_GA(X1, X2, quotS_in_ga(X1, X2))
QUOTT_IN_GA(X1, s(X2)) → QUOTS_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0))))), X2) → U68_GGA(X1, X2, quotT_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0))))), X2) → QUOTT_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), 0) → U69_GGA(X1, quotU_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), 0) → QUOTU_IN_G(X1)
QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → U21_G(X1, quotV_in_g(X1))
QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → QUOTV_IN_G(X1)
QUOTV_IN_G(X1) → U34_G(X1, quotU_in_g(X1))
QUOTV_IN_G(X1) → QUOTU_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), s(X2)) → U70_GGA(X1, X2, quotW_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), s(X2)) → QUOTW_IN_GA(X1, X2)
QUOTW_IN_GA(s(s(s(s(s(s(X1)))))), X2) → U22_GA(X1, X2, quotX_in_ga(X1, X2))
QUOTW_IN_GA(s(s(s(s(s(s(X1)))))), X2) → QUOTX_IN_GA(X1, X2)
QUOTX_IN_GA(X1, 0) → U23_GA(X1, quotU_in_g(X1))
QUOTX_IN_GA(X1, 0) → QUOTU_IN_G(X1)
QUOTX_IN_GA(X1, s(X2)) → U24_GA(X1, X2, quotW_in_ga(X1, X2))
QUOTX_IN_GA(X1, s(X2)) → QUOTW_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0)))))), X2) → U71_GGA(X1, X2, quotX_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0)))))), X2) → QUOTX_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), 0) → U72_GGA(X1, quotY_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), 0) → QUOTY_IN_G(X1)
QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → U25_G(X1, quotZ_in_g(X1))
QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → QUOTZ_IN_G(X1)
QUOTZ_IN_G(X1) → U35_G(X1, quotY_in_g(X1))
QUOTZ_IN_G(X1) → QUOTY_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), s(X2)) → U73_GGA(X1, X2, quotN1_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), s(X2)) → QUOTN1_IN_GA(X1, X2)
QUOTN1_IN_GA(s(s(s(s(s(s(s(X1))))))), X2) → U26_GA(X1, X2, quotN2_in_ga(X1, X2))
QUOTN1_IN_GA(s(s(s(s(s(s(s(X1))))))), X2) → QUOTN2_IN_GA(X1, X2)
QUOTN2_IN_GA(X1, 0) → U27_GA(X1, quotY_in_g(X1))
QUOTN2_IN_GA(X1, 0) → QUOTY_IN_G(X1)
QUOTN2_IN_GA(X1, s(X2)) → U28_GA(X1, X2, quotN1_in_ga(X1, X2))
QUOTN2_IN_GA(X1, s(X2)) → QUOTN1_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(0))))))), X2) → U74_GGA(X1, X2, quotN2_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(0))))))), X2) → QUOTN2_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) → U75_GGA(X1, X2, X3, quotN6_in_ggga(X1, X2, s(s(s(s(s(s(s(X2))))))), X3))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) → QUOTN6_IN_GGGA(X1, X2, s(s(s(s(s(s(s(X2))))))), X3)
QUOTN6_IN_GGGA(X1, 0, X2, 0) → U76_GGGA(X1, X2, quotN3_in_gg(X1, X2))
QUOTN6_IN_GGGA(X1, 0, X2, 0) → QUOTN3_IN_GG(X1, X2)
QUOTN3_IN_GG(s(X1), 0) → U36_GG(X1, quotA_in_g(X1))
QUOTN3_IN_GG(s(X1), 0) → QUOTA_IN_G(X1)
QUOTN3_IN_GG(s(s(X1)), 0) → U37_GG(X1, quotB_in_g(X1))
QUOTN3_IN_GG(s(s(X1)), 0) → QUOTB_IN_G(X1)
QUOTN3_IN_GG(s(s(X1)), s(0)) → U38_GG(X1, quotE_in_g(X1))
QUOTN3_IN_GG(s(s(X1)), s(0)) → QUOTE_IN_G(X1)
QUOTN3_IN_GG(s(s(s(X1))), s(0)) → U39_GG(X1, quotF_in_g(X1))
QUOTN3_IN_GG(s(s(s(X1))), s(0)) → QUOTF_IN_G(X1)
QUOTN3_IN_GG(s(s(s(X1))), s(s(0))) → U40_GG(X1, quotI_in_g(X1))
QUOTN3_IN_GG(s(s(s(X1))), s(s(0))) → QUOTI_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(0))) → U41_GG(X1, quotJ_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(0))) → QUOTJ_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(s(0)))) → U42_GG(X1, quotM_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(s(0)))) → QUOTM_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(0)))) → U43_GG(X1, quotN_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(0)))) → QUOTN_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(s(0))))) → U44_GG(X1, quotQ_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(s(0))))) → QUOTQ_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(0))))) → U45_GG(X1, quotR_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(0))))) → QUOTR_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0)))))) → U46_GG(X1, quotU_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0)))))) → QUOTU_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(0)))))) → U47_GG(X1, quotV_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(0)))))) → QUOTV_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0))))))) → U48_GG(X1, quotY_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0))))))) → QUOTY_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(0))))))) → U49_GG(X1, quotZ_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(0))))))) → QUOTZ_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → U50_GG(X1, X2, quotN4_in_ggg(X1, X2, s(s(s(s(s(s(s(X2)))))))))
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → QUOTN4_IN_GGG(X1, X2, s(s(s(s(s(s(s(X2))))))))
QUOTN4_IN_GGG(X1, 0, X2) → U51_GGG(X1, X2, quotN3_in_gg(X1, X2))
QUOTN4_IN_GGG(X1, 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), 0, X2) → U52_GGG(X1, X2, quotN3_in_gg(X1, X2))
QUOTN4_IN_GGG(s(X1), 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), s(X2), X3) → U53_GGG(X1, X2, X3, quotN4_in_ggg(X1, X2, X3))
QUOTN4_IN_GGG(s(X1), s(X2), X3) → QUOTN4_IN_GGG(X1, X2, X3)
QUOTN6_IN_GGGA(X1, 0, X2, s(X3)) → U77_GGGA(X1, X2, X3, quotN5_in_gga(X1, s(X2), X3))
QUOTN6_IN_GGGA(X1, 0, X2, s(X3)) → QUOTN5_IN_GGA(X1, s(X2), X3)
QUOTN6_IN_GGGA(s(X1), 0, X2, 0) → U78_GGGA(X1, X2, quotN3_in_gg(X1, X2))
QUOTN6_IN_GGGA(s(X1), 0, X2, 0) → QUOTN3_IN_GG(X1, X2)
QUOTN6_IN_GGGA(s(X1), 0, X2, s(X3)) → U79_GGGA(X1, X2, X3, quotN5_in_gga(X1, s(X2), X3))
QUOTN6_IN_GGGA(s(X1), 0, X2, s(X3)) → QUOTN5_IN_GGA(X1, s(X2), X3)
QUOTN6_IN_GGGA(s(X1), s(X2), X3, X4) → U80_GGGA(X1, X2, X3, X4, quotN6_in_ggga(X1, X2, X3, X4))
QUOTN6_IN_GGGA(s(X1), s(X2), X3, X4) → QUOTN6_IN_GGGA(X1, X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
quotN5_in_gga(x1, x2, x3)  =  quotN5_in_gga(x1, x2)
s(x1)  =  s(x1)
0  =  0
quotA_in_g(x1)  =  quotA_in_g(x1)
quotB_in_g(x1)  =  quotB_in_g(x1)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotE_in_g(x1)  =  quotE_in_g(x1)
quotF_in_g(x1)  =  quotF_in_g(x1)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotI_in_g(x1)  =  quotI_in_g(x1)
quotJ_in_g(x1)  =  quotJ_in_g(x1)
quotK_in_ga(x1, x2)  =  quotK_in_ga(x1)
quotL_in_ga(x1, x2)  =  quotL_in_ga(x1)
quotM_in_g(x1)  =  quotM_in_g(x1)
quotN_in_g(x1)  =  quotN_in_g(x1)
quotO_in_ga(x1, x2)  =  quotO_in_ga(x1)
quotP_in_ga(x1, x2)  =  quotP_in_ga(x1)
quotQ_in_g(x1)  =  quotQ_in_g(x1)
quotR_in_g(x1)  =  quotR_in_g(x1)
quotS_in_ga(x1, x2)  =  quotS_in_ga(x1)
quotT_in_ga(x1, x2)  =  quotT_in_ga(x1)
quotU_in_g(x1)  =  quotU_in_g(x1)
quotV_in_g(x1)  =  quotV_in_g(x1)
quotW_in_ga(x1, x2)  =  quotW_in_ga(x1)
quotX_in_ga(x1, x2)  =  quotX_in_ga(x1)
quotY_in_g(x1)  =  quotY_in_g(x1)
quotZ_in_g(x1)  =  quotZ_in_g(x1)
quotN1_in_ga(x1, x2)  =  quotN1_in_ga(x1)
quotN2_in_ga(x1, x2)  =  quotN2_in_ga(x1)
quotN6_in_ggga(x1, x2, x3, x4)  =  quotN6_in_ggga(x1, x2, x3)
quotN3_in_gg(x1, x2)  =  quotN3_in_gg(x1, x2)
quotN4_in_ggg(x1, x2, x3)  =  quotN4_in_ggg(x1, x2, x3)
DIVN7_IN_GGA(x1, x2, x3)  =  DIVN7_IN_GGA(x1, x2)
U81_GGA(x1, x2, x3, x4)  =  U81_GGA(x1, x2, x4)
QUOTN5_IN_GGA(x1, x2, x3)  =  QUOTN5_IN_GGA(x1, x2)
U54_GGA(x1, x2)  =  U54_GGA(x1, x2)
QUOTA_IN_G(x1)  =  QUOTA_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
QUOTB_IN_G(x1)  =  QUOTB_IN_G(x1)
U29_G(x1, x2)  =  U29_G(x1, x2)
U55_GGA(x1, x2, x3)  =  U55_GGA(x1, x3)
QUOTC_IN_GA(x1, x2)  =  QUOTC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)
U3_GA(x1, x2)  =  U3_GA(x1, x2)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U56_GGA(x1, x2, x3)  =  U56_GGA(x1, x3)
U57_GGA(x1, x2)  =  U57_GGA(x1, x2)
QUOTE_IN_G(x1)  =  QUOTE_IN_G(x1)
U5_G(x1, x2)  =  U5_G(x1, x2)
QUOTF_IN_G(x1)  =  QUOTF_IN_G(x1)
U30_G(x1, x2)  =  U30_G(x1, x2)
U58_GGA(x1, x2, x3)  =  U58_GGA(x1, x3)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
QUOTH_IN_GA(x1, x2)  =  QUOTH_IN_GA(x1)
U7_GA(x1, x2)  =  U7_GA(x1, x2)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U59_GGA(x1, x2, x3)  =  U59_GGA(x1, x3)
U60_GGA(x1, x2)  =  U60_GGA(x1, x2)
QUOTI_IN_G(x1)  =  QUOTI_IN_G(x1)
U9_G(x1, x2)  =  U9_G(x1, x2)
QUOTJ_IN_G(x1)  =  QUOTJ_IN_G(x1)
U31_G(x1, x2)  =  U31_G(x1, x2)
U61_GGA(x1, x2, x3)  =  U61_GGA(x1, x3)
QUOTK_IN_GA(x1, x2)  =  QUOTK_IN_GA(x1)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
QUOTL_IN_GA(x1, x2)  =  QUOTL_IN_GA(x1)
U11_GA(x1, x2)  =  U11_GA(x1, x2)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U62_GGA(x1, x2, x3)  =  U62_GGA(x1, x3)
U63_GGA(x1, x2)  =  U63_GGA(x1, x2)
QUOTM_IN_G(x1)  =  QUOTM_IN_G(x1)
U13_G(x1, x2)  =  U13_G(x1, x2)
QUOTN_IN_G(x1)  =  QUOTN_IN_G(x1)
U32_G(x1, x2)  =  U32_G(x1, x2)
U64_GGA(x1, x2, x3)  =  U64_GGA(x1, x3)
QUOTO_IN_GA(x1, x2)  =  QUOTO_IN_GA(x1)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
QUOTP_IN_GA(x1, x2)  =  QUOTP_IN_GA(x1)
U15_GA(x1, x2)  =  U15_GA(x1, x2)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
U65_GGA(x1, x2, x3)  =  U65_GGA(x1, x3)
U66_GGA(x1, x2)  =  U66_GGA(x1, x2)
QUOTQ_IN_G(x1)  =  QUOTQ_IN_G(x1)
U17_G(x1, x2)  =  U17_G(x1, x2)
QUOTR_IN_G(x1)  =  QUOTR_IN_G(x1)
U33_G(x1, x2)  =  U33_G(x1, x2)
U67_GGA(x1, x2, x3)  =  U67_GGA(x1, x3)
QUOTS_IN_GA(x1, x2)  =  QUOTS_IN_GA(x1)
U18_GA(x1, x2, x3)  =  U18_GA(x1, x3)
QUOTT_IN_GA(x1, x2)  =  QUOTT_IN_GA(x1)
U19_GA(x1, x2)  =  U19_GA(x1, x2)
U20_GA(x1, x2, x3)  =  U20_GA(x1, x3)
U68_GGA(x1, x2, x3)  =  U68_GGA(x1, x3)
U69_GGA(x1, x2)  =  U69_GGA(x1, x2)
QUOTU_IN_G(x1)  =  QUOTU_IN_G(x1)
U21_G(x1, x2)  =  U21_G(x1, x2)
QUOTV_IN_G(x1)  =  QUOTV_IN_G(x1)
U34_G(x1, x2)  =  U34_G(x1, x2)
U70_GGA(x1, x2, x3)  =  U70_GGA(x1, x3)
QUOTW_IN_GA(x1, x2)  =  QUOTW_IN_GA(x1)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
QUOTX_IN_GA(x1, x2)  =  QUOTX_IN_GA(x1)
U23_GA(x1, x2)  =  U23_GA(x1, x2)
U24_GA(x1, x2, x3)  =  U24_GA(x1, x3)
U71_GGA(x1, x2, x3)  =  U71_GGA(x1, x3)
U72_GGA(x1, x2)  =  U72_GGA(x1, x2)
QUOTY_IN_G(x1)  =  QUOTY_IN_G(x1)
U25_G(x1, x2)  =  U25_G(x1, x2)
QUOTZ_IN_G(x1)  =  QUOTZ_IN_G(x1)
U35_G(x1, x2)  =  U35_G(x1, x2)
U73_GGA(x1, x2, x3)  =  U73_GGA(x1, x3)
QUOTN1_IN_GA(x1, x2)  =  QUOTN1_IN_GA(x1)
U26_GA(x1, x2, x3)  =  U26_GA(x1, x3)
QUOTN2_IN_GA(x1, x2)  =  QUOTN2_IN_GA(x1)
U27_GA(x1, x2)  =  U27_GA(x1, x2)
U28_GA(x1, x2, x3)  =  U28_GA(x1, x3)
U74_GGA(x1, x2, x3)  =  U74_GGA(x1, x3)
U75_GGA(x1, x2, x3, x4)  =  U75_GGA(x1, x2, x4)
QUOTN6_IN_GGGA(x1, x2, x3, x4)  =  QUOTN6_IN_GGGA(x1, x2, x3)
U76_GGGA(x1, x2, x3)  =  U76_GGGA(x1, x2, x3)
QUOTN3_IN_GG(x1, x2)  =  QUOTN3_IN_GG(x1, x2)
U36_GG(x1, x2)  =  U36_GG(x1, x2)
U37_GG(x1, x2)  =  U37_GG(x1, x2)
U38_GG(x1, x2)  =  U38_GG(x1, x2)
U39_GG(x1, x2)  =  U39_GG(x1, x2)
U40_GG(x1, x2)  =  U40_GG(x1, x2)
U41_GG(x1, x2)  =  U41_GG(x1, x2)
U42_GG(x1, x2)  =  U42_GG(x1, x2)
U43_GG(x1, x2)  =  U43_GG(x1, x2)
U44_GG(x1, x2)  =  U44_GG(x1, x2)
U45_GG(x1, x2)  =  U45_GG(x1, x2)
U46_GG(x1, x2)  =  U46_GG(x1, x2)
U47_GG(x1, x2)  =  U47_GG(x1, x2)
U48_GG(x1, x2)  =  U48_GG(x1, x2)
U49_GG(x1, x2)  =  U49_GG(x1, x2)
U50_GG(x1, x2, x3)  =  U50_GG(x1, x2, x3)
QUOTN4_IN_GGG(x1, x2, x3)  =  QUOTN4_IN_GGG(x1, x2, x3)
U51_GGG(x1, x2, x3)  =  U51_GGG(x1, x2, x3)
U52_GGG(x1, x2, x3)  =  U52_GGG(x1, x2, x3)
U53_GGG(x1, x2, x3, x4)  =  U53_GGG(x1, x2, x3, x4)
U77_GGGA(x1, x2, x3, x4)  =  U77_GGGA(x1, x2, x4)
U78_GGGA(x1, x2, x3)  =  U78_GGGA(x1, x2, x3)
U79_GGGA(x1, x2, x3, x4)  =  U79_GGGA(x1, x2, x4)
U80_GGGA(x1, x2, x3, x4, x5)  =  U80_GGGA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 16 SCCs with 126 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → QUOTZ_IN_G(X1)
QUOTZ_IN_G(X1) → QUOTY_IN_G(X1)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(8) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → QUOTZ_IN_G(X1)
QUOTZ_IN_G(X1) → QUOTY_IN_G(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTZ_IN_G(X1) → QUOTY_IN_G(X1)
    The graph contains the following edges 1 >= 1

  • QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → QUOTZ_IN_G(X1)
    The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTN2_IN_GA(X1, s(X2)) → QUOTN1_IN_GA(X1, X2)
QUOTN1_IN_GA(s(s(s(s(s(s(s(X1))))))), X2) → QUOTN2_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTN1_IN_GA(x1, x2)  =  QUOTN1_IN_GA(x1)
QUOTN2_IN_GA(x1, x2)  =  QUOTN2_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(13) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTN2_IN_GA(X1) → QUOTN1_IN_GA(X1)
QUOTN1_IN_GA(s(s(s(s(s(s(s(X1)))))))) → QUOTN2_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(15) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTN1_IN_GA(s(s(s(s(s(s(s(X1)))))))) → QUOTN2_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • QUOTN2_IN_GA(X1) → QUOTN1_IN_GA(X1)
    The graph contains the following edges 1 >= 1

(16) YES

(17) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → QUOTV_IN_G(X1)
QUOTV_IN_G(X1) → QUOTU_IN_G(X1)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(18) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(19) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → QUOTV_IN_G(X1)
QUOTV_IN_G(X1) → QUOTU_IN_G(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(20) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTV_IN_G(X1) → QUOTU_IN_G(X1)
    The graph contains the following edges 1 >= 1

  • QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → QUOTV_IN_G(X1)
    The graph contains the following edges 1 > 1

(21) YES

(22) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTX_IN_GA(X1, s(X2)) → QUOTW_IN_GA(X1, X2)
QUOTW_IN_GA(s(s(s(s(s(s(X1)))))), X2) → QUOTX_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTW_IN_GA(x1, x2)  =  QUOTW_IN_GA(x1)
QUOTX_IN_GA(x1, x2)  =  QUOTX_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(23) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTX_IN_GA(X1) → QUOTW_IN_GA(X1)
QUOTW_IN_GA(s(s(s(s(s(s(X1))))))) → QUOTX_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(25) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTW_IN_GA(s(s(s(s(s(s(X1))))))) → QUOTX_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • QUOTX_IN_GA(X1) → QUOTW_IN_GA(X1)
    The graph contains the following edges 1 >= 1

(26) YES

(27) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTQ_IN_G(s(s(s(s(s(X1)))))) → QUOTR_IN_G(X1)
QUOTR_IN_G(X1) → QUOTQ_IN_G(X1)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(28) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTQ_IN_G(s(s(s(s(s(X1)))))) → QUOTR_IN_G(X1)
QUOTR_IN_G(X1) → QUOTQ_IN_G(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(30) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTR_IN_G(X1) → QUOTQ_IN_G(X1)
    The graph contains the following edges 1 >= 1

  • QUOTQ_IN_G(s(s(s(s(s(X1)))))) → QUOTR_IN_G(X1)
    The graph contains the following edges 1 > 1

(31) YES

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTT_IN_GA(X1, s(X2)) → QUOTS_IN_GA(X1, X2)
QUOTS_IN_GA(s(s(s(s(s(X1))))), X2) → QUOTT_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTS_IN_GA(x1, x2)  =  QUOTS_IN_GA(x1)
QUOTT_IN_GA(x1, x2)  =  QUOTT_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTT_IN_GA(X1) → QUOTS_IN_GA(X1)
QUOTS_IN_GA(s(s(s(s(s(X1)))))) → QUOTT_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTS_IN_GA(s(s(s(s(s(X1)))))) → QUOTT_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • QUOTT_IN_GA(X1) → QUOTS_IN_GA(X1)
    The graph contains the following edges 1 >= 1

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTM_IN_G(s(s(s(s(X1))))) → QUOTN_IN_G(X1)
QUOTN_IN_G(X1) → QUOTM_IN_G(X1)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTM_IN_G(s(s(s(s(X1))))) → QUOTN_IN_G(X1)
QUOTN_IN_G(X1) → QUOTM_IN_G(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(40) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTN_IN_G(X1) → QUOTM_IN_G(X1)
    The graph contains the following edges 1 >= 1

  • QUOTM_IN_G(s(s(s(s(X1))))) → QUOTN_IN_G(X1)
    The graph contains the following edges 1 > 1

(41) YES

(42) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTP_IN_GA(X1, s(X2)) → QUOTO_IN_GA(X1, X2)
QUOTO_IN_GA(s(s(s(s(X1)))), X2) → QUOTP_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTO_IN_GA(x1, x2)  =  QUOTO_IN_GA(x1)
QUOTP_IN_GA(x1, x2)  =  QUOTP_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(43) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTP_IN_GA(X1) → QUOTO_IN_GA(X1)
QUOTO_IN_GA(s(s(s(s(X1))))) → QUOTP_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(45) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTO_IN_GA(s(s(s(s(X1))))) → QUOTP_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • QUOTP_IN_GA(X1) → QUOTO_IN_GA(X1)
    The graph contains the following edges 1 >= 1

(46) YES

(47) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTI_IN_G(s(s(s(X1)))) → QUOTJ_IN_G(X1)
QUOTJ_IN_G(X1) → QUOTI_IN_G(X1)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(48) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(49) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTI_IN_G(s(s(s(X1)))) → QUOTJ_IN_G(X1)
QUOTJ_IN_G(X1) → QUOTI_IN_G(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(50) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTJ_IN_G(X1) → QUOTI_IN_G(X1)
    The graph contains the following edges 1 >= 1

  • QUOTI_IN_G(s(s(s(X1)))) → QUOTJ_IN_G(X1)
    The graph contains the following edges 1 > 1

(51) YES

(52) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTL_IN_GA(X1, s(X2)) → QUOTK_IN_GA(X1, X2)
QUOTK_IN_GA(s(s(s(X1))), X2) → QUOTL_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTK_IN_GA(x1, x2)  =  QUOTK_IN_GA(x1)
QUOTL_IN_GA(x1, x2)  =  QUOTL_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(53) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(54) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTL_IN_GA(X1) → QUOTK_IN_GA(X1)
QUOTK_IN_GA(s(s(s(X1)))) → QUOTL_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(55) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTK_IN_GA(s(s(s(X1)))) → QUOTL_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • QUOTL_IN_GA(X1) → QUOTK_IN_GA(X1)
    The graph contains the following edges 1 >= 1

(56) YES

(57) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTE_IN_G(s(s(X1))) → QUOTF_IN_G(X1)
QUOTF_IN_G(X1) → QUOTE_IN_G(X1)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(58) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(59) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTE_IN_G(s(s(X1))) → QUOTF_IN_G(X1)
QUOTF_IN_G(X1) → QUOTE_IN_G(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(60) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTF_IN_G(X1) → QUOTE_IN_G(X1)
    The graph contains the following edges 1 >= 1

  • QUOTE_IN_G(s(s(X1))) → QUOTF_IN_G(X1)
    The graph contains the following edges 1 > 1

(61) YES

(62) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTH_IN_GA(X1, s(X2)) → QUOTG_IN_GA(X1, X2)
QUOTG_IN_GA(s(s(X1)), X2) → QUOTH_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)
QUOTH_IN_GA(x1, x2)  =  QUOTH_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(63) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(64) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTH_IN_GA(X1) → QUOTG_IN_GA(X1)
QUOTG_IN_GA(s(s(X1))) → QUOTH_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(65) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTG_IN_GA(s(s(X1))) → QUOTH_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • QUOTH_IN_GA(X1) → QUOTG_IN_GA(X1)
    The graph contains the following edges 1 >= 1

(66) YES

(67) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTA_IN_G(s(X1)) → QUOTB_IN_G(X1)
QUOTB_IN_G(X1) → QUOTA_IN_G(X1)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(68) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(69) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTA_IN_G(s(X1)) → QUOTB_IN_G(X1)
QUOTB_IN_G(X1) → QUOTA_IN_G(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(70) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTB_IN_G(X1) → QUOTA_IN_G(X1)
    The graph contains the following edges 1 >= 1

  • QUOTA_IN_G(s(X1)) → QUOTB_IN_G(X1)
    The graph contains the following edges 1 > 1

(71) YES

(72) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → QUOTN4_IN_GGG(X1, X2, s(s(s(s(s(s(s(X2))))))))
QUOTN4_IN_GGG(X1, 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), s(X2), X3) → QUOTN4_IN_GGG(X1, X2, X3)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(73) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(74) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → QUOTN4_IN_GGG(X1, X2, s(s(s(s(s(s(s(X2))))))))
QUOTN4_IN_GGG(X1, 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), s(X2), X3) → QUOTN4_IN_GGG(X1, X2, X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(75) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTN4_IN_GGG(s(X1), s(X2), X3) → QUOTN4_IN_GGG(X1, X2, X3)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → QUOTN4_IN_GGG(X1, X2, s(s(s(s(s(s(s(X2))))))))
    The graph contains the following edges 1 > 1, 2 > 2, 2 >= 3

  • QUOTN4_IN_GGG(X1, 0, X2) → QUOTN3_IN_GG(X1, X2)
    The graph contains the following edges 1 >= 1, 3 >= 2

  • QUOTN4_IN_GGG(s(X1), 0, X2) → QUOTN3_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 3 >= 2

(76) YES

(77) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTD_IN_GA(X1, s(X2)) → QUOTC_IN_GA(X1, X2)
QUOTC_IN_GA(s(X1), X2) → QUOTD_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTC_IN_GA(x1, x2)  =  QUOTC_IN_GA(x1)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(78) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(79) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTD_IN_GA(X1) → QUOTC_IN_GA(X1)
QUOTC_IN_GA(s(X1)) → QUOTD_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(80) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTC_IN_GA(s(X1)) → QUOTD_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • QUOTD_IN_GA(X1) → QUOTC_IN_GA(X1)
    The graph contains the following edges 1 >= 1

(81) YES

(82) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) → QUOTN6_IN_GGGA(X1, X2, s(s(s(s(s(s(s(X2))))))), X3)
QUOTN6_IN_GGGA(X1, 0, X2, s(X3)) → QUOTN5_IN_GGA(X1, s(X2), X3)
QUOTN6_IN_GGGA(s(X1), 0, X2, s(X3)) → QUOTN5_IN_GGA(X1, s(X2), X3)
QUOTN6_IN_GGGA(s(X1), s(X2), X3, X4) → QUOTN6_IN_GGGA(X1, X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
QUOTN5_IN_GGA(x1, x2, x3)  =  QUOTN5_IN_GGA(x1, x2)
QUOTN6_IN_GGGA(x1, x2, x3, x4)  =  QUOTN6_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(83) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(84) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2))))))))) → QUOTN6_IN_GGGA(X1, X2, s(s(s(s(s(s(s(X2))))))))
QUOTN6_IN_GGGA(X1, 0, X2) → QUOTN5_IN_GGA(X1, s(X2))
QUOTN6_IN_GGGA(s(X1), 0, X2) → QUOTN5_IN_GGA(X1, s(X2))
QUOTN6_IN_GGGA(s(X1), s(X2), X3) → QUOTN6_IN_GGGA(X1, X2, X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(85) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTN6_IN_GGGA(s(X1), s(X2), X3) → QUOTN6_IN_GGGA(X1, X2, X3)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2))))))))) → QUOTN6_IN_GGGA(X1, X2, s(s(s(s(s(s(s(X2))))))))
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

  • QUOTN6_IN_GGGA(X1, 0, X2) → QUOTN5_IN_GGA(X1, s(X2))
    The graph contains the following edges 1 >= 1

  • QUOTN6_IN_GGGA(s(X1), 0, X2) → QUOTN5_IN_GGA(X1, s(X2))
    The graph contains the following edges 1 > 1

(86) YES